#include "util/util.h"
#include "decomp/decomp.h"
#include <vector>
#include <cstdlib>
#include <iostream>
using std::vector;

static void fun2minterm( unsigned vsize , unsigned fun , vector<unsigned short> & onset )
{
   for( unsigned i = 0 , j = 1 ; i < (1<<vsize) ; ++ i , j = j << 1 )
      if( fun & j ) 
         onset.push_back( i );
}
static void mincube( unsigned vsize , unsigned fun , vector<unsigned> & primes )
{
   extern void quine_mccluskey( vector<unsigned short> & onset , vector<unsigned> & prime );

   vector<unsigned short> minterms;
   fun2minterm( vsize , fun, minterms );
   quine_mccluskey( minterms , primes );
}
static void cube2unsat_bind( unsigned c , unsigned s, uint8_t onset , Unsat_bind & u )
{
   int ncnt=0;

   u.push_back( Bind(0xFF,onset?0:1,s) ); // if onset value is 0 
   for( unsigned i = 0 ; i < s ; ++ i , c=c>>2 )
      switch( c&3){ 
         case 0: u.push_back( Bind( i , 0 , s ) ); u[0][i] = ncnt , u.back()[i] = ncnt ++ ; break;
         case 1: u.push_back( Bind( i , 1 , s) ); u[0][i] = ncnt , u.back()[i] = ncnt ++ ; break;
         case 2: break;
      } 
}
static void report( const vector< Unsat_bind > & u ){
   for( unsigned i = 0 ; i < u.size() ; ++ i )u[i].print();
}
int main( int argc , const char ** argv)
{
   ArgAnalyzer arg( "gen_decomp <int:vsize> <hex:fun> <string:file>" , argc , argv );
   
   vector< Unsat_bind > onbind , offbind;
   {
      // compute the minimal cube 
      vector<unsigned> onset , offset;
      unsigned vsize = atoi(arg[0].c_str()) ;
      {
         unsigned fun   = strtol( arg[1].c_str() , 0 , 0 ) ;
         mincube( vsize , fun , onset );
         mincube( vsize , (~fun) , offset );
      }   
      onbind.resize( onset.size() );
      offbind.resize( offset.size() );
      // backwark derive the decomposing frame 
      for( unsigned i = 0 ; i < onset.size() ; ++i ) 
         cube2unsat_bind( onset[i] , vsize , 1 , onbind[i] );
      for( unsigned i = 0 ;i < offset.size() ; ++ i )
         cube2unsat_bind( offset[i] , vsize , 0 , offbind[i] );
   }
   
   //for( unsigned i = 0 ; i < vsize ; ++ i )
   {
      // find the frame contain i and reconstruct next unsat binding
      
      // at the meanwhile construct the interpolant binding 
   }
}
